﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Eco.ObjectRepresentation;
using CommonClasses.Logger;
using CommonClasses.Model;
using CommandLists.Model;
using System.IO;
using System.Diagnostics;
using CommonClasses.Utility;
using Eco.Services;
using System.Windows.Forms;

namespace CommandListsVerifier
{
    /// <summary>
    /// Верификатор Списков команд
    /// </summary>
    public class CLVerifier
    {

        /// <summary>
        /// Провайдер сервисов ECO
        /// </summary>
        private IEcoServiceProvider ecoServiceProvider;

        /// <summary>
        /// Загрузчик описания данных для верификации
        /// </summary>
        private VerifierDomainModelLoader verDMLoader;

        /// <summary>
        /// Логгер
        /// </summary>
        private ILogger logger;

        /// <summary>
        /// Представляет собой структуру из узлов верификации и описания команд СК
        /// </summary>
        private VerifierDomainModel verDM;

        /// <summary>
        /// Все узлы
        /// </summary>
        private List<Node> allNodes = new List<Node>();

        /// <summary>
        /// Количество свойств
        /// </summary>
        public int SpecCount = 14;

        /// <summary>
        /// Массив с текстом спецификаций
        /// </summary>
        public string[] SpecStrings;

        /// <summary>
        /// Комментарии к спецификациям
        /// </summary>
        public string[] SpecComments;

        /// <summary>
        /// Конструктор верификатора СК
        /// </summary>
        /// <param name="ecoServiceProvider">Провайдер сервисов ECO</param>
        /// <param name="logger">Логгер</param>
        public CLVerifier(IEcoServiceProvider ecoServiceProvider, ILogger logger)
        {
            this.ecoServiceProvider = ecoServiceProvider;
            this.logger = logger;
            this.verDMLoader = new VerifierDomainModelLoader(ecoServiceProvider);

            this.verDM = verDMLoader.LoadVerifierDMFromfile();
            this.verDM.CommandsDescriptors.ForEach(
                cd => cd.Actions.ForEach(
                    act =>
                    {
                        if (allNodes.Find(nod => nod.OldID == act.Node.OldID) == null)
                            allNodes.Add(act.Node);
                    }));

            /*
            var verDM = new VerifierDomainModel();
            verDM.CommandsDescriptors = new List<CommandDescriptor>();
            verDM.CommandsDescriptors.Add(
                new CommandDescriptor{
                   Actions = new List<Action>(), CommandID = "0"}
            );
            verDM.CommandsDescriptors[0].Actions.Add(
                new Action
                {
                    Asynchronous = true,
                    DSt = 0,
                    Name = "name1",
                    Node = null,
                    TargetParamName = "123",
                    TargetState = 0
                }
                );
            verDMLoader.SaveVerifierDMTofile(verDM);
             */

        }

        /// <summary>
        /// Сгенерить код на вход верификатору
        /// </summary>
        private ErrorReport GenerateSMVCode(string filename, IEnumerable<CommandList> lists)
        {
            ErrorReport errorReport = new ErrorReport(ecoServiceProvider);
            PathUtility.RestoreCurrentDirectory(Locality.ExeFile);
            Environment.CurrentDirectory = Path.GetDirectoryName(filename);
            FileStream stream = File.Open(Path.GetFileName(filename), FileMode.Create, FileAccess.Write);
            if (stream == null)
            {
                errorReport.AddError("Ошибка создания файла верифицируемой модели (NuSMV\\input.smv)", new EcoExtensions.Model.EcoPoint(ecoServiceProvider, new System.Drawing.Point()), null);
                return errorReport;
            }
            StreamWriter writer = new StreamWriter(stream);

            // код для каждого из модулей + 2 модуля счетчика тактов + main
            // каждый модуль расчитан на код для соответствующего узла
            // очевидно, что на каждом такте код генерится не для каждого узла
            // поскольку команда списка команд расчитана на определенные узлы устройства, зачастую, вообще на один узел
            int modulesCount = allNodes.Count();
            int allModulesCount = allNodes.Count() + 3;
            int tactCounterModuleIndex = modulesCount;
            int cycleCounterModuleIndex = modulesCount + 1;
            int mainModuleIndex = modulesCount + 2;

            string[] modulesCode = new string[allModulesCount]; // собствено коды модулей. Внимание, модуль TactCounter разбит на два (т.к. генерировать будем параллельно для двух переменных)

            // следующие массивы используются для разрешения проблем с генерацией кода для асинхронных команд
            string[] modulesAsyncCode1 = new string[allModulesCount]; // выполняется ли модулем асинхронная команда
            string[] modulesAsyncCode2 = new string[allModulesCount];
            int[] modulesAsyncCodeTact = new int[allModulesCount];

            #region Начало модулей

            bool isFirstModule; // только для того, чтобы не получилось кода: <...>(, st1, st2)

            modulesCode[mainModuleIndex] = "\r\nMODULE main \r\nVAR tactCounter : process MTactCounter(";
            modulesCode[tactCounterModuleIndex] = "\r\n-- Счетчик тактов \r\nMODULE MTactCounter(";

            isFirstModule = true;
            for (int i = 0; i < modulesCount; i++)
            {
                modulesAsyncCode1[i] = "";
                modulesAsyncCode2[i] = "";
                modulesAsyncCodeTact[i] = 0;

                modulesCode[i] = "\r\n-- " + allNodes[i].Name + "\r\nMODULE Module" + i + "(tact_num, cycle_num)" + "\r\nVAR st : 0..100; \r\nASSIGN\r\n    init(st) := 0;\r\n    next(st) :=\r\n     case";

                modulesCode[tactCounterModuleIndex] += (!isFirstModule ? ", " : "") + "st" + i;
                modulesCode[mainModuleIndex] += (!isFirstModule ? ", " : "") + "m" + i + ".st";
                isFirstModule = false;
            }

            modulesCode[mainModuleIndex] += ");";
            modulesCode[tactCounterModuleIndex] += ") \r\nVAR tact_num : 0..300; cycle_num : 0..300;" + "\r\nASSIGN \r\n    init(tact_num) := 1;\r\n    init(cycle_num) := 0;\r\n    next(tact_num) :=\r\n    case";

            // код модуля MTactCounter разобъем на два элемента массива, т.к. будем венсти учет состояний двух переменных: tact_num и cycle_num
            modulesCode[cycleCounterModuleIndex] += "\r\n    next(cycle_num) :=\r\n    case";

            #endregion

            #region Основная часть модулей
            int tactCount = lists.ElementAt(0).CommandSequence.Count; // кол-во тактов
            int clCount = lists.Count(); // кол-во СК
            int cycle_num = 0;          // на какой мы итерации цикла, на 2-ом можем находиться только для устранения проблем с генерацией кода асинхронных действий
            int lastCycleParam = 0;     // последний параметр повторения цикла
            int lastCycleBeginTact = 0; // последний такт, где начался цикл

            // по всем тактам
            for (int tact = 0; tact < tactCount; tact++)
            {
                Command nextCommand = tact < tactCount - 1 ? lists.ElementAt(0).CommandSequence[tact + 1] : null; // нужно для геренерации условия окончания цикла, делается на такте перед реальным окончанием цикла, поэтому читаем след. команду заранее
                CommandDescriptor nextCommandDescriptor = null;
                if (nextCommand != null)
                    nextCommandDescriptor = verDM.CommandsDescriptors.Find(cd => cd.CommandID == nextCommand.OldID);

                string tactCounterString = "\r\n       tact_num  = " + (tact + 1); // код, сгенеренный на данном такте для модуля tactCounter1 (для удобства так нужно, эту строку, возможно, будем дважды использовать)

                // по всем СК (на данном такте)
                for (int i = 0; i < clCount; i++)
                {
                    Command command = lists.ElementAt(i).CommandSequence[tact]; // command - команда списка команд i на такте tact
                    var allCommands = ecoServiceProvider.GetEcoService<IOclService>().Evaluate("Command.allInstances").GetAsIList<Command>();
                    /*
                    var goodCommands = from c in allCommands
                                       where c.OldID != ""
                                       select c;
                    var badCommands = from c in allCommands
                                      where c.OldID == ""
                                      select c;
                     */
                    CommandDescriptor commandDescriptor = verDM.CommandsDescriptors.Find(cd => cd.CommandID == command.OldID); // дескриптор command
                    if (commandDescriptor != null) // нашли дескриптор (нпр. это точно не "Простой")
                    {
                        // начало цикла?
                        if (commandDescriptor.SpecCommandType == CommandDescriptor.SpecialCommandType.CycleBegin)
                        {
                            if (cycle_num < 2)
                            {
                                lastCycleParam = command.Parameters[0].DefaultValue;

                                // отдельно отлавливаем ситуацию, когда параметр цикла равен 0
                                if (lastCycleParam == 0)
                                {
                                    int k;
                                    for (k = 0; k < tactCount; k++)
                                    {
                                        Command command1 = lists.ElementAt(i).CommandSequence[k];
                                        CommandDescriptor commandDescriptor1 = verDM.CommandsDescriptors.Find(cd => cd.CommandID == command1.OldID);
                                        if ((commandDescriptor1 != null) && (commandDescriptor1.SpecCommandType == CommandDescriptor.SpecialCommandType.CycleEnd))
                                            break; // т.к. считаем, что НЦ соответствует хотя бы один КЦ, то цикл остановится именно здесь
                                    }
                                    tact = k;
                                    break;
                                }
                                cycle_num = 1;
                                lastCycleBeginTact = tact;
                                modulesCode[cycleCounterModuleIndex] += "\r\n       tact_num  = " + (tact + 1) + " : (cycle_num + 1) mod 300;";
                                break;
                            }
                            else for (int k = 0; k < modulesCount; k++)
                                {
                                    if (modulesAsyncCodeTact[k] != 0)
                                    {
                                        modulesAsyncCodeTact[k] = tact + 1;
                                    }
                                }
                        }
                        // конец цикла?
                        else if (commandDescriptor.SpecCommandType == CommandDescriptor.SpecialCommandType.CycleEnd)
                        {
                            if ((cycle_num < lastCycleParam) && (cycle_num < 2))
                            {
                                cycle_num++;
                                modulesCode[cycleCounterModuleIndex] += "\r\n       tact_num  = " + (tact + 1) + " : 0;";
                                tact = lastCycleBeginTact - 1;
                            }
                            else
                            {
                                cycle_num = 0;
                                modulesCode[cycleCounterModuleIndex] += "\r\n       tact_num  = " + (tact + 1) + " : 0;";
                            }
                            break;
                        }
                        // нормальная команда
                        else
                        {
                            commandDescriptor.Actions.ForEach(
                               act =>
                               {
                                   Node node = allNodes.Find(n => n.OldID == act.Node.OldID);
                                   int nodeIndex = allNodes.IndexOf(node);
                                   int targetState = act.TargetParamName == "" ? // возможно, нам нужно добавить ожидание определенного состояния одного из модулей для перехода такта в следующий из данного
                                       act.TargetState
                                       :
                                       (command.Parameters.Find(par => par.Name == act.TargetParamName)).DefaultValue;

                                   // Если команда синхронная
                                   if (!act.Asynchronous)
                                   {
                                       // если до этого была асинхронная
                                       if (modulesAsyncCodeTact[nodeIndex] != 0)
                                       {
                                           string cycleString;
                                           if (cycle_num == 0)
                                               cycleString = "";
                                           else if (cycle_num == 1)
                                               cycleString = " & cycle_num = 1";
                                           else cycleString = " & cycle_num > 1";

                                           modulesCode[nodeIndex] += "\r\n       tact_num >= " + modulesAsyncCodeTact[nodeIndex] + " & tact_num <= " + (tact + 1) + cycleString + modulesAsyncCode1[nodeIndex] +
                                                                     "\r\n       tact_num >= " + modulesAsyncCodeTact[nodeIndex] + " & tact_num <= " + (tact + 1) + cycleString + modulesAsyncCode2[nodeIndex];

                                           modulesAsyncCode1[nodeIndex] = "";
                                           modulesAsyncCode2[nodeIndex] = "";
                                           modulesAsyncCodeTact[nodeIndex] = 0;
                                       }

                                       // ожидаем в модуле и в TactCounter прихода в целевое состояние
                                       // на втором проходе это не нужно, поскольку код генерится только для асинхронных
                                       if (cycle_num < 2)
                                       {

                                           tactCounterString += " & st" + nodeIndex + " = " + targetState;
                                           if (act.DSt != 0)
                                               modulesCode[nodeIndex] += "\r\n       tact_num  = " + (tact + 1) + " & st < " + targetState + " : st + " + act.DSt + ";" +
                                                                         "\r\n       tact_num  = " + (tact + 1) + " & st > " + targetState + " : st - " + act.DSt + ";";
                                       }
                                   }
                                   else
                                   {
                                       if (modulesAsyncCodeTact[nodeIndex] != 0)
                                       {
                                           string cycleString;
                                           if (cycle_num == 0)
                                               cycleString = "";
                                           else if (cycle_num == 1)
                                               cycleString = " & cycle_num = 1";
                                           else cycleString = " & cycle_num > 1";

                                           modulesCode[nodeIndex] += "\r\n       tact_num >= " + modulesAsyncCodeTact[nodeIndex] + " & tact_num <= " + (tact + 1) + cycleString + modulesAsyncCode1[nodeIndex] +
                                                                     "\r\n       tact_num >= " + modulesAsyncCodeTact[nodeIndex] + " & tact_num <= " + (tact + 1) + cycleString + modulesAsyncCode2[nodeIndex];
                                       }

                                       if (cycle_num == 1)
                                       {
                                           modulesAsyncCode1[nodeIndex] = " & st < " + targetState + " : st + " + act.DSt + ";";
                                           modulesAsyncCode2[nodeIndex] = " & st > " + targetState + " : st - " + act.DSt + ";";
                                       }
                                       else if (cycle_num > 1)
                                       {
                                           modulesAsyncCode1[nodeIndex] = " & st < " + targetState + " : st + " + act.DSt + ";";
                                           modulesAsyncCode2[nodeIndex] = " & st > " + targetState + " : st - " + act.DSt + ";";
                                       }
                                       else
                                       {
                                           modulesAsyncCode1[nodeIndex] = " & st < " + targetState + " : st + " + act.DSt + ";";
                                           modulesAsyncCode2[nodeIndex] = " & st > " + targetState + " : st - " + act.DSt + ";";
                                       }
                                       modulesAsyncCodeTact[nodeIndex] = tact + 1;
                                   }

                                   if (nextCommandDescriptor != null)
                                   {
                                       // следующая команда - начало цикла?
                                       if (nextCommandDescriptor.SpecCommandType == CommandDescriptor.SpecialCommandType.CycleBegin)
                                       {
                                           if (modulesAsyncCodeTact[nodeIndex] != 0)
                                           {
                                               modulesCode[nodeIndex] += "\r\n       tact_num >= " + modulesAsyncCodeTact[nodeIndex] + " & tact_num <= " + (tact + 1) + modulesAsyncCode1[nodeIndex] +
                                                                         "\r\n       tact_num >= " + modulesAsyncCodeTact[nodeIndex] + " & tact_num <= " + (tact + 1) + modulesAsyncCode2[nodeIndex];
                                               modulesAsyncCodeTact[nodeIndex] = tact + 2;
                                           }
                                       }
                                   }
                               }
                                ); // commandDescriptor.Actions.ForEach
                        }
                    }
                }

                // если на следующем такте конец цикла, то генерим код соответствующий для tactCounter:
                // т.е. либо переходим на след.  такт, либо на начало цикла
                if ((cycle_num < 2) && (nextCommandDescriptor != null) && (nextCommandDescriptor.SpecCommandType == CommandDescriptor.SpecialCommandType.CycleEnd))
                {
                    modulesCode[tactCounterModuleIndex] += tactCounterString + " & cycle_num < " + lastCycleParam + " : " + (lastCycleBeginTact + 1) + ";";
                    modulesCode[tactCounterModuleIndex] += tactCounterString + " & cycle_num = " + lastCycleParam + " : " + (tact + 2) + ";";
                }
                else if (cycle_num < 2)
                {
                    modulesCode[tactCounterModuleIndex] += tactCounterString + " : " + (tact + 2) + ";";
                }
            }
            #endregion

            #region Окончание модулей

            // добавить окончание модуля MTactCounter
            modulesCode[tactCounterModuleIndex] += " \r\n       1 : tact_num;\r\n    esac;\r\n";
            modulesCode[cycleCounterModuleIndex] += "\r\n       1 : cycle_num;\r\n    esac; \r\nFAIRNESS running \r\n";

            // добавить окончание всех модулей узлов
            for (int i = 0; i < modulesCount; i++)
            {
                if (modulesAsyncCode1[i] != "")
                {
                    string cycleString;
                    if (cycle_num == 0)
                        cycleString = "";
                    else if (cycle_num == 1)
                        cycleString = " & cycle_num = 1";
                    else cycleString = " & cycle_num > 1";

                    modulesCode[i] += "\r\n       tact_num >= " + modulesAsyncCodeTact[i] + " & tact_num <= " + (tactCount) + cycleString + modulesAsyncCode1[i] +
                                      "\r\n       tact_num >= " + modulesAsyncCodeTact[i] + " & tact_num <= " + (tactCount) + cycleString + modulesAsyncCode1[i];

                    modulesAsyncCode1[i] = "";
                    modulesAsyncCode2[i] = "";
                }
                modulesCode[i] += "\r\n       1 : st;\r\n    esac;\r\nFAIRNESS running\r\n";

                modulesCode[mainModuleIndex] += "\r\n    m" + i + " : process Module" + i + "(tactCounter.tact_num, tactCounter.cycle_num);";
            }

            modulesCode[mainModuleIndex] += "\r\nFAIRNESS running";
            #endregion

            // Итоговая строка всего кода
            string resString = "";

            // Соединение кода всех модулей
            for (int i = 0; i < allModulesCount; i++)
                resString += modulesCode[i];

            SpecComments = new string[SpecCount];
            SpecStrings = new string[SpecCount];

            SpecComments[0] = "Обнаружена возможность столкновения при повороте выдвинутой руки робота МП-9С с опорой портального робота";
            SpecStrings[0] = "AG (((m3.st = 0 & m1.st = 1) -> AX !(m3.st = 1)) & ((m3.st = 1 & m1.st = 1) -> AX !(m3.st = 0)))";

            SpecComments[1] = "Обнаружена возможность столкновения при повороте выдвинутой нижней руки робота МП-11 с опорой портального робота";
            SpecStrings[1] = "AG (((m6.st = 0 & m11.st = 1) -> AX !(m6.st = 1)) & ((m6.st = 1 & m11.st = 1) -> AX !(m6.st = 0)))";

            SpecComments[2] = "Обнаружена возможность столкновения при повороте выдвинутой верхней руки робота МП-11 с бортиками лотка-ската";
            SpecStrings[2] = "AG (((m6.st = 0 & m9.st = 1) -> AX !(m6.st = 1)) & ((m6.st = 1 & m9.st = 1) -> AX !(m6.st = 0)))";

            SpecComments[3] = "Обнаружена возможность столкновения заготовки, зажатой схватом выдвинутой верхней руки робота МП-11, с бортиками лотка при развороте заготовки в горизонтальное положение";
            SpecStrings[3] = "AG ((m6.st = 1 & m9.st = 1 & m7.st = 0) -> AX ! (m7.st = 1))";

            SpecComments[4] = "Обнаружена возможность столкновения заготовки, зажатой схватом верхней руки робота МП-11, с ограничителем лотка-ската в нижнем положении при движении руки назад";
            SpecStrings[4] = "AG ((m6.st = 1 & m5.st = 0 & m9.st = 1 & m10.st = 0) -> AX !(m9.st = 0))";

            SpecComments[5] = "Обнаружена возможность столкновения закрытого схвата верхней руки робота МП-11 с заготовкой в лотке при движении руки вперед в нижнем положении";
            SpecStrings[5] = "AG ((m6.st = 1 & m5.st = 0 & m9.st = 0 & m10.st = 0) -> AX !(m9.st = 1))";

            SpecComments[6] = "Обнаружена возможность столкновения схвата нижней руки робота МП-11 с установочным элементом приспособления при движении руки в нижнем положении";
            SpecStrings[6] = "AG ((m6.st = 1 & m5.st = 0 & m11.st = 0) -> AX !(m11.st = 1)) & ((m6.st = 1 & m5.st = 0 & m11.st = 1) -> AX !(m11.st = 0))";

            SpecComments[7] = "Обнаружена возможность столкновения закрытого схвата нижней руки робота МП-11 с заготовкой в трубчатом лотке при движении руки вперед в нижнем положении";
            SpecStrings[7] = "AG ((m6.st = 0 & m5.st = 0 & m12.st = 0 & m8.st = 0 & m11.st = 0) -> AX !(m11.st = 1))";


            SpecComments[8] = "Обнаружена возможность столкновения схвата нижней руки робота МП-11 в верхнем положении с трубчатым лотком";
            SpecStrings[8] = "AG !((m6.st = 0 & m11.st = 1 & m12.st = 1) | (m6.st = 0 & m11.st = 1 & m5.st = 1))";

            SpecComments[9] = "Обнаружена возможность столкновения схвата портального робота со схватом робота МП-9C";
            SpecStrings[9] = "AG !(m13.st >= 70 & m13.st <= 90 & m3.st = 0 & m1.st = 1)";

            SpecComments[10] = "Обнаружена возможность столкновения схвата портального робота со схватом нижней руки МП-11";
            SpecStrings[10] = "AG !(m13.st >= 0 & m13.st <= 20 & m6.st = 1 & m11.st = 1)";

            SpecComments[11] = "Обнаружена возможность столкновения схвата выдвинутой нижней руки робота МП-11 в нижнем положении с зажимами закрытого приспособления";
            SpecStrings[11] = "AG !(m6.st = 1 & m5.st = 0 & m11.st = 1 & m0.st = 0)";

            SpecComments[12] = "Обнаружена возможность столкновения схвата робота МП-9С со столом портального робота при выдвинутой вперед руке в нижнем положении";
            SpecStrings[12] = "AG !(m3.st = 0 & m2.st = 0 & m1.st = 1)";

            SpecComments[13] = "Обнаружена возможность зависания управляющей программы и недостижение ее конечного такта";
            SpecStrings[13] = "AG (EF tactCounter.tact_num = " + (tactCount + 1) + ")";

            // добавляем свойства
            resString +=
@"

-- 0  Клешни
-- 1  МП-9C.Рука
-- 2  МП-9C.Стол.Поднятие
-- 3  МП-9C.Стол.Поворот
-- 4  МП-9C.Схват
-- 5  МП11.Стол.Поднятие
-- 6  МП11.Стол.Поворот
-- 7  МП11.Верхняя Рука.Схват.Поворот
-- 8  МП11.Нижняя Рука.Схват
-- 9  МП11.Верхняя Рука
-- 10 МП11.Верхняя Рука.Схват
-- 11 МП11.Нижняя Рука
-- 12 МП11.Нижняя Рука.Схват.Поднятие
-- 13 Портальный робот.Платформа
-- 14 Портальный робот.Схват
-- 15 Портальный робот.Схват.Поднятие
-- 16 Счетчик тактов 
";

            for (int i = 0; i < SpecCount; i++)
                resString += (SpecStrings[i] != ""? "\r\nSPEC " :  "\r\n") + SpecStrings[i] + "\r\n";

            writer.Write(resString);
            writer.Flush();
            writer.Close();
            stream.Close();

            return errorReport;
        }        


        /// <summary>
        /// Верифицировать список команд
        /// </summary>
        /// <param name="lists">Список команд</param>
        /// <returns>
        /// Список ошибок верификации
        /// </returns>
        public ErrorReport Verify(IEnumerable<CommandList> lists)
        {

            var report = new ErrorReport(ecoServiceProvider);
            if (lists.Count() == 0)
                return report;

            report.AddRange(GenerateSMVCode("NuSMV\\input.smv", lists));

            PathUtility.RestoreCurrentDirectory(Locality.ExeFile);
            Environment.CurrentDirectory = "NuSMV";

            var info = new ProcessStartInfo("NuSMV.exe", "-int input.smv");
            info.RedirectStandardInput = true;
            info.RedirectStandardOutput = true;
            info.UseShellExecute = false;
            info.CreateNoWindow = true;
            var proc = Process.Start(info);
            StreamWriter procStreamWriter = proc.StandardInput;
            StreamReader procStreamReader = proc.StandardOutput;
            procStreamWriter.WriteLine("go");            
            StreamReader outTxtReader;
            string s1;
            s1 = procStreamReader.ReadLine();
            s1 = procStreamReader.ReadLine();
            s1 = procStreamReader.ReadLine();
            s1 = procStreamReader.ReadLine();
            s1 = procStreamReader.ReadLine();
            s1 = procStreamReader.ReadLine();
            s1 = procStreamReader.ReadLine();
            s1 = procStreamReader.ReadLine();
            s1 = procStreamReader.ReadLine();            

            for (int i = 0; i < SpecCount; i++)
            {
                //procStreamReader.DiscardBufferedData();                
                procStreamWriter.WriteLine("check_ctlspec -o out.txt -n " + i);
                s1 = procStreamReader.ReadLine();                                
                procStreamWriter.WriteLine("show_traces -o trace.xml -p 4");
                procStreamWriter.WriteLine("echo");
                s1 = procStreamReader.ReadLine();                
                                
                outTxtReader = new StreamReader("out.txt");

                string s = null;
                s = outTxtReader.ReadLine();
                if (s.EndsWith("is true"))
                {
                    outTxtReader.Close();
                    continue;
                }
                
                string comments = SpecComments[i];

                int tact_num, cycle_num;
                
                GetErrorTactCycleFromXMLTrace(out tact_num, out cycle_num);

                if ((i == SpecCount - 1)&&(cycle_num == 0))
                    report.AddError(comments, new EcoExtensions.Model.EcoPoint(ecoServiceProvider, new System.Drawing.Point(0, 0)), null);
                else report.AddError(comments + " (такт " + tact_num + (cycle_num != 0 ? ", цикл " + cycle_num + ")" : "" + ")"), new EcoExtensions.Model.EcoPoint(ecoServiceProvider, new System.Drawing.Point(0, 0)), null);

                outTxtReader.Close();                

                break;
            }                                                                     
                        
            procStreamWriter.WriteLine("quit");                        
            proc.WaitForExit(20000);
            if (!proc.HasExited)
            {
                proc.Kill();
            }
            proc.Close();

            return report;
        }

        /// <summary>
        /// Получить из файла трейса номер ошибочного такта и счетчик цикла
        /// </summary>
        /// <param name="tact_num">Номер такта</param>
        /// <param name="cycle_num">Номер цикла</param>
        private void GetErrorTactCycleFromXMLTrace(out int tact_num, out int cycle_num)
        {
            CounterExample.counterexample ce = SerializationUtility.DeserializeFromFile<CounterExample.counterexample>("trace.xml");
            int lastNodeIndex = ce.node.Count<CounterExample.counterexampleNode>() - 1;
            CounterExample.counterexampleNodeState ceState = ce.node[lastNodeIndex].state[0];
            string t = null, c = null;
            foreach (var variable in ceState.value)
            {
                if ((variable.variable == "tactCounter.tact_num") & (t == null))
                    t = variable.Value;
                else if ((variable.variable == "tactCounter.cycle_num") & (c == null))
                    c = variable.Value;

                if ((c != null) & (t != null))
                    break;
            };
            tact_num = int.Parse(t);
            cycle_num = int.Parse(c);
        }
    }
}
